%jml
The Java Modeling Language (JML) is a behavioral interface 
specification language~\cite{jml-paper} tailored to Java. Thus, JML serves to describe contracts with static information that appear in Java declarations and how they act. JML specifications are written in the form of \textit{special annotation} comments that are inserted directly in source code of programs. These comments must begin with an at-sign (\code{@}) and can be written in two ways: by using \code{//@ ...} or \code{/*@ ... @*/}. The following fragment shows contracts for a class \code{Person}~\cite{jml-dbc}.

\begin{lstlisting}[frame=single,framerule=0pt,numbers=none]
public class Person {
  //@ public model int weight;
  //@ public model String name;
  
  private String _name; 
  private int _weight;
  
  //@ private represents name <- _name;
  //@ private represents weight <- _weight;

  //@ public invariant !name.equals("") && 
  //@                  weight >= 0; 
		                                       
  //@ ensures \result == weight;
  public /*@ pure @*/ int getWeight() { .. }	
		
  /*@ requires kgs > 0;
    @ assignable weight;     														
    @ ensures weight == \old(weight + kgs); 
    @*/   				
   public void addKgs(int kgs) { .. }
}
\end{lstlisting}
% && weight + kgs >= 0;

The \code{\textbf{model}} modifier introduces specification-only fields, also called \textit{model fields}. A model field should be thought of as an abstraction of a set of concrete fields used in the implementation of this type and its subtypes~\cite{jml-reference}. In the class \code{Person}, we have two model fields, i.e. \code{name} and \code{weight}, representing (via \code{\textbf{represents}} clause) the concrete attributes \code{\_name} and \code{\_weight}, respectively.

The \code{\textbf{invariant}} clause defines predicates that are true in all visible states of objects of a class. The invariant in the example has public visibility and establishes that the value of attribute \code{\_name} is different from an empty string and the value of \code{\_weight} is greater than or equal to zero. 

Also, JML uses the \code{requires} clause to specify the obligations of the caller of a method, what must be true to call a method. For instance, the precondition of the method \code{addKgs} insists on the added value to be greater than zero. A postcondition specifies the implementor's obligation, what must be true at the end of a method, just before it returns to the caller. In JML, the \code{ensures} clause introduces a postcondition. In the example, it asserts the value of the attribute \code{\_weight} at the end of the method \code{addKgs} is equal to the value of the expression \code{$\backslash$old(weight + kgs)}. By using the \code{$\backslash$old} operator we can refer to the value of an expression in the pre-state of a method.

The \code{assignable} clause gives a frame axiom for a specification. Only locations named and their associations can be assigned during method execution. In method \code{addKgs}, we state that only \code{weight} is changeable. The JML modifier \code{pure} indicates that the method doesn't have any side effects and hence can appear in specifications.